﻿// Jinx AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Core;

namespace Formality.FormalSystem.Reasoning.FunctionSubstitution
{
    public class Search : IJustificationSearch
    {
        public Search(Proposition From, Proposition To)
            : this(From, To, true)
        { }

        public Search(Proposition From, Proposition To, bool ContextSensitive)
        {
            if (ContextSensitive)
                this.ContextSensitive = ContextSensitive;

            this.From = From;
            this.To = To;
            SubstitutionMap = new SubstitutionMap();
        }

        public SubstitutionMap SubstitutionMap { get; private set; }

        public Justification Perform()
        {
            if (IsSubstitution(From, To))
            {
                if (TypeCheck(From))
                    return new Justification(this);
            }

            return null;
        }

        #region IJustificationSearch Members

        Reasoning.Justification IJustificationSearch.Perform()
        {
            return Perform();
        }

        #endregion

        internal Search(Proposition From, Proposition To, Search Search)
        {
            this.From = From;
            this.To = To;
            this.ContextSensitive = Search.ContextSensitive;
            this.SubstitutionMap = new SubstitutionMap(Search.SubstitutionMap);
        }

        internal Search(Search Search)
        {
            this.From = Search.From;
            this.To = Search.To;
            this.ContextSensitive = Search.ContextSensitive;
            this.SubstitutionMap = new SubstitutionMap(Search.SubstitutionMap);
        }

        private bool ContextSensitive;
        private Proposition From, To;
        private IDictionary<Variable, Variable> BoundVariableMap = new Dictionary<Variable, Variable>();

        private bool IsSubstitution(Proposition f, Proposition t)
        {
            if (f.Type == PropType.Function)
            {
                f = MapBoundVariables(f);

                if (AdmitSubstitution(new Function(f), t, Predicate))
                    return true;
            }
            else
            {
                var Binder = (f.Type == PropType.Binder) && (t.Type == PropType.Binder);

                if (Binder) MapBoundVariable(f, t);

                f = MapBoundVariables(f);

                if (f.Operator == t.Operator)
                    if (f.Variables.SequenceEqual(t.Variables, (v1, v2) => v1.Name == v2.Name))
                        if (f.Operands.SequenceEqual(t.Operands,
                                                     (o1, o2) => IsSubstitution(o1, o2)))
                        {
                            if (Binder) UnmapBoundVariable(f);
                            return true;
                        }
            }

            return false;
        }

        private void UnmapBoundVariable(Proposition f)
        {
            var fVar = new Binder(f).Variable;

            BoundVariableMap.Remove(fVar);
        }

        private void MapBoundVariable(Proposition f, Proposition t)
        {
            var fVar = new Binder(f).Variable;
            var tVar = new Binder(t).Variable;

            BoundVariableMap[fVar] = tVar;
        }

        private Proposition MapBoundVariables(Proposition p)
        {
            return new Proposition(p, v =>
            {
                Variable v2;
                return BoundVariableMap.TryGetValue(v, out v2) ? v2 : v;
            }, op => op);
        }

        private bool AdmitSubstitution(Function From, Proposition To, BinaryPredicate<Proposition> Comparison)
        {
            var QName = From.Name;

            if (QName.Bound)
                return (From.Proposition == To);

            Substitution Sub;

            if (SubstitutionMap.TryGetValue(QName, out Sub))
            {
                var Expansion = Sub.Expand(From);

                if (Expansion == null)
                    return false;

                return Comparison(Expansion, To);
            }

            SubstitutionMap[QName] = new Substitution(From, To);
            return NoNamesCaptured(From, To);
        }

        /*
         * This looks for variable capture and returns true if it occurs. 
         */
        private bool NoNamesCaptured(Function From, Proposition p)
        {
            var IntroducedVariables = p.FreeVariables().Except(From.Arguments);

            return IntroducedVariables.All(v => v.Free);
        }

        private BinaryPredicate<Proposition> Predicate
        {
            get
            {
                if (ContextSensitive)
                    return (p1, p2) => p1 == p2;
                else
                    return (p1, p2) => p1.ToString() == p2.ToString();
            }
        }

        private bool TypeCheck(Proposition From)
        {
            return !ReplacesArguments(From);
        }

        private bool ReplacesArguments(Proposition p)
        {
            return false;
            if (p.Type == PropType.Function)
            {
                var f = new Function(p);

                if (f.Arguments.Any(arg => SubstitutionMap.HasSubstitution(arg)))
                    return true;
            }

            return p.Operands.Any(o => ReplacesArguments(o));
        }
    }
}
